COMMENT ⊗   VALID 00003 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	There is a large area of contemporary mathematics which can be profitably
 00003 00003	
 00004 ENDMK
⊗;
There is a large area of contemporary mathematics which can be profitably
explored using an interactive first-order theorem prover.  This report
will describe #   applications of the the Stanford A.I. Project's theorem prover. 

The first application explores the field of Euclidean Geometry.  
The second example deals with abstract algebra, in particular, Implicative models.
Third, we used some of the programmable features of the prover to give a solution 
to a puzzle.